Termination of the given ITRSProblem could not be shown:



↳ ITRS

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

eval(i, j) → Cond_eval(&&(&&(>=@z(-@z(i, j), 1@z), >=@z(nat, 0@z)), >@z(pos, 0@z)), i, j, nat, pos)
Cond_eval(TRUE, i, j, nat, pos) → eval(-@z(i, nat), +@z(j, pos))

The set Q consists of the following terms:

eval(x0, x1)
Cond_eval(TRUE, x0, x1, x2, x3)